YES 30.645
↳ HASKELL
↳ LR
((plusFM :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap b a -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
\oldnew→new
addToFM0 old new = new
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
((plusFM :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap b a -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: a -> b -> FiniteMap a b
|
import qualified FiniteMap import qualified Prelude |
case fm_l of EmptyFM → True Branch left_key _ _ _ _ →
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
left_ok0 fm_l key EmptyFM = True left_ok0 fm_l key (Branch left_key _ _ _ _) =
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
case fm_r of EmptyFM → True Branch right_key _ _ _ _ →
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
right_ok0 fm_r key EmptyFM = True right_ok0 fm_r key (Branch right_key _ _ _ _) =
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
case fm_R of Branch _ _ _ fm_rl fm_rr
| sizeFM fm_rl < 2 * sizeFM fm_rr
→ single_L fm_L fm_R | otherwise
→ double_L fm_L fm_R
mkBalBranch0 fm_L fm_R (Branch _ _ _ fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
case fm_L of Branch _ _ _ fm_ll fm_lr
| sizeFM fm_lr < 2 * sizeFM fm_ll
→ single_R fm_L fm_R | otherwise
→ double_R fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch _ _ _ fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
((plusFM :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
fm_l@(Branch yy yz zu zv zw)
Branch yy yz zu zv zw
fm_r@(Branch zy zz vuu vuv vuw)
Branch zy zz vuu vuv vuw
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
((plusFM :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) |
import qualified Maybe import qualified Prelude |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap a b) where |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap a b -> (a,b)
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord a => FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
splitLT EmptyFM split_key = emptyFM splitLT (Branch key elt xw fm_l fm_r) split_key
| split_key < key
= splitLT fm_l split_key | split_key > key
= mkVBalBranch key elt fm_l (splitLT fm_r split_key) | otherwise
= fm_l
splitLT EmptyFM split_key = splitLT4 EmptyFM split_key splitLT (Branch key elt xw fm_l fm_r) split_key = splitLT3 (Branch key elt xw fm_l fm_r) split_key
splitLT0 key elt xw fm_l fm_r split_key True = fm_l
splitLT2 key elt xw fm_l fm_r split_key True = splitLT fm_l split_key splitLT2 key elt xw fm_l fm_r split_key False = splitLT1 key elt xw fm_l fm_r split_key (split_key > key)
splitLT1 key elt xw fm_l fm_r split_key True = mkVBalBranch key elt fm_l (splitLT fm_r split_key) splitLT1 key elt xw fm_l fm_r split_key False = splitLT0 key elt xw fm_l fm_r split_key otherwise
splitLT3 (Branch key elt xw fm_l fm_r) split_key = splitLT2 key elt xw fm_l fm_r split_key (split_key < key)
splitLT4 EmptyFM split_key = emptyFM splitLT4 vyu vyv = splitLT3 vyu vyv
splitGT EmptyFM split_key = emptyFM splitGT (Branch key elt xx fm_l fm_r) split_key
| split_key > key
= splitGT fm_r split_key | split_key < key
= mkVBalBranch key elt (splitGT fm_l split_key) fm_r | otherwise
= fm_r
splitGT EmptyFM split_key = splitGT4 EmptyFM split_key splitGT (Branch key elt xx fm_l fm_r) split_key = splitGT3 (Branch key elt xx fm_l fm_r) split_key
splitGT2 key elt xx fm_l fm_r split_key True = splitGT fm_r split_key splitGT2 key elt xx fm_l fm_r split_key False = splitGT1 key elt xx fm_l fm_r split_key (split_key < key)
splitGT1 key elt xx fm_l fm_r split_key True = mkVBalBranch key elt (splitGT fm_l split_key) fm_r splitGT1 key elt xx fm_l fm_r split_key False = splitGT0 key elt xx fm_l fm_r split_key otherwise
splitGT0 key elt xx fm_l fm_r split_key True = fm_r
splitGT3 (Branch key elt xx fm_l fm_r) split_key = splitGT2 key elt xx fm_l fm_r split_key (split_key > key)
splitGT4 EmptyFM split_key = emptyFM splitGT4 vyy vyz = splitGT3 vyy vyz
mkVBalBranch key elt EmptyFM fm_r = addToFM fm_r key elt mkVBalBranch key elt fm_l EmptyFM = addToFM fm_l key elt mkVBalBranch key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
| sIZE_RATIO * size_l < size_r
= mkBalBranch zy zz (mkVBalBranch key elt (Branch yy yz zu zv zw) vuv) vuw | sIZE_RATIO * size_r < size_l
= mkBalBranch yy yz zv (mkVBalBranch key elt zw (Branch zy zz vuu vuv vuw)) | otherwise
= mkBranch 13 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw) where
size_l = sizeFM (Branch yy yz zu zv zw)
size_r = sizeFM (Branch zy zz vuu vuv vuw)
mkVBalBranch key elt EmptyFM fm_r = mkVBalBranch5 key elt EmptyFM fm_r mkVBalBranch key elt fm_l EmptyFM = mkVBalBranch4 key elt fm_l EmptyFM mkVBalBranch key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw) = mkVBalBranch3 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
mkVBalBranch3 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw) =
mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * size_l < size_r) where
mkVBalBranch0 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBranch 13 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch yy yz zv (mkVBalBranch key elt zw (Branch zy zz vuu vuv vuw)) mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch0 key elt yy yz zu zv zw zy zz vuu vuv vuw otherwise
mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch zy zz (mkVBalBranch key elt (Branch yy yz zu zv zw) vuv) vuw mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch yy yz zu zv zw)
size_r = sizeFM (Branch zy zz vuu vuv vuw)
mkVBalBranch4 key elt fm_l EmptyFM = addToFM fm_l key elt mkVBalBranch4 vzx vzy vzz wuu = mkVBalBranch3 vzx vzy vzz wuu
mkVBalBranch5 key elt EmptyFM fm_r = addToFM fm_r key elt mkVBalBranch5 wuw wux wuy wuz = mkVBalBranch4 wuw wux wuy wuz
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr otherwise
mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch key elt fm_L fm_R
| size_l + size_r < 2
= mkBranch 1 key elt fm_L fm_R | size_r > sIZE_RATIO * size_l
= mkBalBranch0 fm_L fm_R fm_R | size_l > sIZE_RATIO * size_r
= mkBalBranch1 fm_L fm_R fm_L | otherwise
= mkBranch 2 key elt fm_L fm_R where
double_L fm_l (Branch key_r elt_r vvx (Branch key_rl elt_rl vvy fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vvv fm_ll (Branch key_lr elt_lr vvw fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
| sizeFM fm_rl < 2 * sizeFM fm_rr
= single_L fm_L fm_R | otherwise
= double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
| sizeFM fm_lr < 2 * sizeFM fm_ll
= single_R fm_L fm_R | otherwise
= double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r vww fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vux fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R
mkBalBranch6 key elt fm_L fm_R =
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2) where
double_L fm_l (Branch key_r elt_r vvx (Branch key_rl elt_rl vvy fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vvv fm_ll (Branch key_lr elt_lr vvw fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vww fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vux fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
addToFM_C combiner EmptyFM key elt = unitFM key elt addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt
| new_key < key
= mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r | new_key > key
= mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt) | otherwise
= Branch new_key (combiner elt new_elt) size fm_l fm_r
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt) addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)
addToFM_C4 combiner EmptyFM key elt = unitFM key elt addToFM_C4 wvy wvz wwu wwv = addToFM_C3 wvy wvz wwu wwv
undefined
| False
= undefined
undefined = undefined1
undefined0 True = undefined
undefined1 = undefined0 False
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
((plusFM :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) |
import qualified Maybe import qualified Prelude |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
addToFM_C :: Ord a => (b -> b -> b) -> FiniteMap a b -> a -> b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
emptyFM :: FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sIZE_RATIO :: Int
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
sizeFM :: FiniteMap b a -> Int
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
splitLT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2) where
double_L fm_l (Branch key_r elt_r vvx (Branch key_rl elt_rl vvy fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vvv fm_ll (Branch key_lr elt_lr vvw fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr True = single_L fm_L fm_R mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vvz vwu vwv fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vvz vwu vwv fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr True = single_R fm_L fm_R mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vuy vuz vvu fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vuy vuz vvu fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vww fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vux fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R
mkBalBranch6Size_r www wwx wwy wwz = sizeFM www
mkBalBranch6MkBalBranch2 www wwx wwy wwz key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch6Double_R www wwx wwy wwz (Branch key_l elt_l vvv fm_ll (Branch key_lr elt_lr vvw fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 wwx wwy fm_lrr fm_r)
mkBalBranch6Single_R www wwx wwy wwz (Branch key_l elt_l vux fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 wwx wwy fm_lr fm_r)
mkBalBranch6MkBalBranch00 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr True = mkBalBranch6Double_L www wwx wwy wwz fm_L fm_R
mkBalBranch6MkBalBranch10 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr True = mkBalBranch6Double_R www wwx wwy wwz fm_L fm_R
mkBalBranch6Single_L www wwx wwy wwz fm_l (Branch key_r elt_r vww fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 wwx wwy fm_l fm_rl) fm_rr
mkBalBranch6MkBalBranch12 www wwx wwy wwz fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch6MkBalBranch11 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch6MkBalBranch02 www wwx wwy wwz fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch6MkBalBranch01 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch6Double_L www wwx wwy wwz fm_l (Branch key_r elt_r vvx (Branch key_rl elt_rl vvy fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 wwx wwy fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
mkBalBranch6MkBalBranch11 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr True = mkBalBranch6Single_R www wwx wwy wwz fm_L fm_R mkBalBranch6MkBalBranch11 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr False = mkBalBranch6MkBalBranch10 www wwx wwy wwz fm_L fm_R vuy vuz vvu fm_ll fm_lr otherwise
mkBalBranch6MkBalBranch5 www wwx wwy wwz key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R mkBalBranch6MkBalBranch5 www wwx wwy wwz key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 www wwx wwy wwz key elt fm_L fm_R (mkBalBranch6Size_r www wwx wwy wwz > sIZE_RATIO * mkBalBranch6Size_l www wwx wwy wwz)
mkBalBranch6Size_l www wwx wwy wwz = sizeFM wwz
mkBalBranch6MkBalBranch1 www wwx wwy wwz fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr) = mkBalBranch6MkBalBranch12 www wwx wwy wwz fm_L fm_R (Branch vuy vuz vvu fm_ll fm_lr)
mkBalBranch6MkBalBranch4 www wwx wwy wwz key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 www wwx wwy wwz fm_L fm_R fm_R mkBalBranch6MkBalBranch4 www wwx wwy wwz key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 www wwx wwy wwz key elt fm_L fm_R (mkBalBranch6Size_l www wwx wwy wwz > sIZE_RATIO * mkBalBranch6Size_r www wwx wwy wwz)
mkBalBranch6MkBalBranch3 www wwx wwy wwz key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 www wwx wwy wwz fm_L fm_R fm_L mkBalBranch6MkBalBranch3 www wwx wwy wwz key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 www wwx wwy wwz key elt fm_L fm_R otherwise
mkBalBranch6MkBalBranch01 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr True = mkBalBranch6Single_L www wwx wwy wwz fm_L fm_R mkBalBranch6MkBalBranch01 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr False = mkBalBranch6MkBalBranch00 www wwx wwy wwz fm_L fm_R vvz vwu vwv fm_rl fm_rr otherwise
mkBalBranch6MkBalBranch0 www wwx wwy wwz fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr) = mkBalBranch6MkBalBranch02 www wwx wwy wwz fm_L fm_R (Branch vvz vwu vwv fm_rl fm_rr)
let
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r in result where
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True left_ok0 fm_l key (Branch left_key wu wv ww wx) =
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True right_ok0 fm_r key (Branch right_key vw vx vy vz) =
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
right_size = sizeFM fm_r
unbox x = x
mkBranchUnbox wxu wxv wxw x = x
mkBranchLeft_size wxu wxv wxw = sizeFM wxu
mkBranchRight_ok wxu wxv wxw = mkBranchRight_ok0 wxu wxv wxw wxv wxw wxv
mkBranchLeft_ok0 wxu wxv wxw fm_l key EmptyFM = True mkBranchLeft_ok0 wxu wxv wxw fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key
mkBranchRight_ok0 wxu wxv wxw fm_r key EmptyFM = True mkBranchRight_ok0 wxu wxv wxw fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r
mkBranchLeft_ok wxu wxv wxw = mkBranchLeft_ok0 wxu wxv wxw wxu wxw wxu
mkBranchBalance_ok wxu wxv wxw = True
mkBranchRight_size wxu wxv wxw = sizeFM wxv
let
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r in result
mkBranchResult wxx wxy wxz wyu = Branch wxx wxy (mkBranchUnbox wxz wyu wxx (1 + mkBranchLeft_size wxz wyu wxx + mkBranchRight_size wxz wyu wxx)) wxz wyu
mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * size_l < size_r) where
mkVBalBranch0 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBranch 13 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch yy yz zv (mkVBalBranch key elt zw (Branch zy zz vuu vuv vuw)) mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch0 key elt yy yz zu zv zw zy zz vuu vuv vuw otherwise
mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch zy zz (mkVBalBranch key elt (Branch yy yz zu zv zw) vuv) vuw mkVBalBranch2 key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch1 key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch yy yz zu zv zw)
size_r = sizeFM (Branch zy zz vuu vuv vuw)
mkVBalBranch3MkVBalBranch0 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBranch 13 key elt (Branch yy yz zu zv zw) (Branch zy zz vuu vuv vuw)
mkVBalBranch3Size_r wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy = sizeFM (Branch wyv wyw wyx wyy wyz)
mkVBalBranch3MkVBalBranch2 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch zy zz (mkVBalBranch key elt (Branch yy yz zu zv zw) vuv) vuw mkVBalBranch3MkVBalBranch2 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch3MkVBalBranch1 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw (sIZE_RATIO * mkVBalBranch3Size_r wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy < mkVBalBranch3Size_l wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy)
mkVBalBranch3Size_l wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy = sizeFM (Branch wzu wzv wzw wzx wzy)
mkVBalBranch3MkVBalBranch1 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw True = mkBalBranch yy yz zv (mkVBalBranch key elt zw (Branch zy zz vuu vuv vuw)) mkVBalBranch3MkVBalBranch1 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw False = mkVBalBranch3MkVBalBranch0 wyv wyw wyx wyy wyz wzu wzv wzw wzx wzy key elt yy yz zu zv zw zy zz vuu vuv vuw otherwise
mkVBalBranch split_key elt1 (plusFM lts left) (plusFM gts right) where
gts = splitGT fm1 split_key
lts = splitLT fm1 split_key
plusFMLts wzz xuu = splitLT wzz xuu
plusFMGts wzz xuu = splitGT wzz xuu
let
biggest_left_key = fst (findMax fm_l) in biggest_left_key < key
mkBranchLeft_ok0Biggest_left_key xuv = fst (findMax xuv)
let
smallest_right_key = fst (findMin fm_r) in key < smallest_right_key
mkBranchRight_ok0Smallest_right_key xuw = fst (findMin xuw)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
((plusFM :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) |
import qualified Maybe import qualified Prelude |
|||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||
addToFM :: Ord a => FiniteMap a b -> a -> b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
emptyFM :: FiniteMap b a
|
|||||||||||||
findMax :: FiniteMap b a -> (b,a)
|
|||||||||||||
findMin :: FiniteMap a b -> (a,b)
|
|||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranch :: Ord b => Int -> b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranchUnbox :: Ord a => -> (FiniteMap a b) ( -> (FiniteMap a b) ( -> a (Int -> Int)))
|
|||||||||||||
mkVBalBranch :: Ord b => b -> a -> FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||
sizeFM :: FiniteMap a b -> Int
|
|||||||||||||
splitGT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
(plusFM :: FiniteMap Char a -> FiniteMap Char a -> FiniteMap Char a) |
import qualified Maybe import qualified Prelude |
|||||||||||||
data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a) |
|||||||||||||
instance (Eq a, Eq b) => Eq (FiniteMap b a) where |
|||||||||||||
addToFM :: Ord b => FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
addToFM_C :: Ord b => (a -> a -> a) -> FiniteMap b a -> b -> a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
emptyFM :: FiniteMap a b
|
|||||||||||||
findMax :: FiniteMap a b -> (a,b)
|
|||||||||||||
findMin :: FiniteMap b a -> (b,a)
|
|||||||||||||
mkBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranch :: Ord a => Int -> a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
mkBranchUnbox :: Ord a => -> (FiniteMap a b) ( -> (FiniteMap a b) ( -> a (Int -> Int)))
|
|||||||||||||
mkVBalBranch :: Ord a => a -> b -> FiniteMap a b -> FiniteMap a b -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
plusFM :: Ord b => FiniteMap b a -> FiniteMap b a -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
sIZE_RATIO :: Int
|
|||||||||||||
sizeFM :: FiniteMap b a -> Int
|
|||||||||||||
splitGT :: Ord b => FiniteMap b a -> b -> FiniteMap b a
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
splitLT :: Ord a => FiniteMap a b -> a -> FiniteMap a b
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
|
|||||||||||||
unitFM :: b -> a -> FiniteMap b a
|
import qualified FiniteMap import qualified Prelude |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_esEs(Succ(xux65200), Succ(xux64700)) → new_esEs(xux65200, xux64700)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_esEs0(Succ(xux286000), Succ(xux281000)) → new_esEs0(xux286000, xux281000)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_primMinusNat(Succ(xux756000), Succ(xux753000)) → new_primMinusNat(xux756000, xux753000)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_primPlusNat(Succ(xux2100), Succ(xux160)) → new_primPlusNat(xux2100, xux160)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
new_addToFM_C2(xux647, xux648, xux649, Branch(xux6500, xux6501, xux6502, xux6503, xux6504), xux651, xux652, xux653, True, bb, bc) → new_addToFM_C2(xux6500, xux6501, xux6502, xux6503, xux6504, xux652, xux653, new_lt(xux652, xux6500, bb), bb, bc)
new_addToFM_C2(xux647, xux648, xux649, xux650, xux651, xux652, xux653, False, bb, bc) → new_addToFM_C1(xux647, xux648, xux649, xux650, xux651, xux652, xux653, new_gt(xux652, xux647, bb), bb, bc)
new_addToFM_C1(xux665, xux666, xux667, xux668, xux669, xux670, xux671, True, h, ba) → new_addToFM_C(xux669, xux670, xux671, h, ba)
new_addToFM_C2(xux647, xux648, xux649, xux650, xux651, xux652, xux653, True, bb, bc) → new_addToFM_C(xux650, xux652, xux653, bb, bc)
new_addToFM_C(Branch(xux6500, xux6501, xux6502, xux6503, xux6504), xux652, xux653, bb, bc) → new_addToFM_C2(xux6500, xux6501, xux6502, xux6503, xux6504, xux652, xux653, new_lt(xux652, xux6500, bb), bb, bc)
new_esEs9(Pos(Succ(xux65200)), Neg(xux65000)) → new_esEs2
new_gt(xux652, xux647, ty_Int) → new_gt0(xux652, xux647)
new_lt(xux652, xux6500, ty_Float) → error([])
new_esEs8 → False
new_esEs9(Pos(Zero), Pos(Succ(xux650000))) → new_esEs1(Zero, Succ(xux650000))
new_gt(xux652, xux647, ty_Integer) → error([])
new_gt0(Neg(Zero), Pos(Succ(xux64700))) → new_esEs7
new_gt0(Pos(Succ(xux65200)), Neg(xux6470)) → new_esEs6
new_esEs9(Pos(Zero), Neg(Succ(xux650000))) → new_esEs2
new_esEs5(Succ(xux65200), Zero) → new_esEs6
new_lt(xux652, xux6500, app(app(app(ty_@3, bf), bg), bh)) → error([])
new_gt0(Neg(Zero), Neg(Succ(xux64700))) → new_esEs5(Succ(xux64700), Zero)
new_esEs5(Zero, Zero) → new_esEs8
new_esEs9(Pos(Zero), Pos(Zero)) → new_esEs4
new_gt(xux652, xux647, app(ty_Maybe, be)) → error([])
new_gt(Char(xux6520), Char(xux6470), ty_Char) → new_esEs5(xux6520, xux6470)
new_lt(xux652, xux6500, ty_Int) → new_lt1(xux652, xux6500)
new_gt(xux652, xux647, ty_Float) → error([])
new_gt0(Neg(Zero), Neg(Zero)) → new_esEs8
new_lt1(xux652, xux6500) → new_esEs9(xux652, xux6500)
new_esEs9(Neg(Zero), Neg(Succ(xux650000))) → new_esEs1(Succ(xux650000), Zero)
new_esEs3 → True
new_gt(xux652, xux647, ty_Double) → error([])
new_esEs9(Neg(Succ(xux65200)), Pos(xux65000)) → new_esEs3
new_lt0(Char(xux400), Char(xux500)) → new_esEs1(xux400, xux500)
new_esEs9(Neg(Zero), Pos(Succ(xux650000))) → new_esEs3
new_gt0(Pos(Zero), Neg(Zero)) → new_esEs8
new_gt0(Neg(Zero), Pos(Zero)) → new_esEs8
new_gt(xux652, xux647, app(app(app(ty_@3, bf), bg), bh)) → error([])
new_lt(xux652, xux6500, app(app(ty_Either, ca), cb)) → error([])
new_lt(xux652, xux6500, app(app(ty_@2, cd), ce)) → error([])
new_esEs9(Pos(Succ(xux65200)), Pos(xux65000)) → new_esEs1(Succ(xux65200), xux65000)
new_gt(xux652, xux647, app(ty_[], cc)) → error([])
new_esEs2 → False
new_esEs1(Succ(xux286000), Succ(xux281000)) → new_esEs1(xux286000, xux281000)
new_gt(xux652, xux647, ty_Ordering) → error([])
new_gt(xux652, xux647, ty_@0) → error([])
new_esEs9(Neg(Zero), Neg(Zero)) → new_esEs4
new_gt(xux652, xux647, app(ty_Ratio, bd)) → error([])
new_lt(xux652, xux6500, app(ty_Ratio, bd)) → error([])
new_lt(xux652, xux6500, ty_Ordering) → error([])
new_esEs9(Pos(Zero), Neg(Zero)) → new_esEs4
new_esEs5(Succ(xux65200), Succ(xux64700)) → new_esEs5(xux65200, xux64700)
new_esEs9(Neg(Zero), Pos(Zero)) → new_esEs4
new_lt(xux652, xux6500, app(ty_Maybe, be)) → error([])
new_gt(xux652, xux647, ty_Bool) → error([])
new_lt(xux652, xux6500, ty_Integer) → error([])
new_gt0(Pos(Zero), Pos(Zero)) → new_esEs8
new_gt0(Pos(Succ(xux65200)), Pos(xux6470)) → new_esEs5(Succ(xux65200), xux6470)
new_esEs7 → False
new_gt0(Pos(Zero), Pos(Succ(xux64700))) → new_esEs5(Zero, Succ(xux64700))
new_esEs4 → False
new_esEs5(Zero, Succ(xux64700)) → new_esEs7
new_lt(xux652, xux6500, ty_Char) → new_lt0(xux652, xux6500)
new_lt(xux652, xux6500, ty_Bool) → error([])
new_lt(xux652, xux6500, app(ty_[], cc)) → error([])
new_esEs1(Zero, Zero) → new_esEs4
new_esEs1(Succ(xux286000), Zero) → new_esEs2
new_gt(xux652, xux647, app(app(ty_@2, cd), ce)) → error([])
new_gt0(Neg(Succ(xux65200)), Neg(xux6470)) → new_esEs5(xux6470, Succ(xux65200))
new_esEs9(Neg(Succ(xux65200)), Neg(xux65000)) → new_esEs1(xux65000, Succ(xux65200))
new_gt0(Pos(Zero), Neg(Succ(xux64700))) → new_esEs6
new_gt0(Neg(Succ(xux65200)), Pos(xux6470)) → new_esEs7
new_esEs6 → True
new_lt(xux652, xux6500, ty_@0) → error([])
new_lt(xux652, xux6500, ty_Double) → error([])
new_gt(xux652, xux647, app(app(ty_Either, ca), cb)) → error([])
new_esEs1(Zero, Succ(xux281000)) → new_esEs3
new_gt0(Pos(Succ(x0)), Pos(x1))
new_esEs7
new_esEs3
new_lt(x0, x1, ty_@0)
new_lt(x0, x1, ty_Float)
new_esEs5(Succ(x0), Zero)
new_lt(x0, x1, app(ty_Ratio, x2))
new_esEs9(Neg(Zero), Pos(Succ(x0)))
new_gt(x0, x1, ty_Int)
new_esEs9(Pos(Zero), Neg(Succ(x0)))
new_gt(x0, x1, ty_Bool)
new_gt(x0, x1, ty_@0)
new_gt(x0, x1, app(app(ty_@2, x2), x3))
new_gt(x0, x1, ty_Float)
new_lt(x0, x1, ty_Bool)
new_esEs4
new_esEs9(Neg(Succ(x0)), Pos(x1))
new_esEs9(Pos(Succ(x0)), Neg(x1))
new_gt0(Neg(Zero), Pos(Zero))
new_gt0(Pos(Zero), Neg(Zero))
new_lt(x0, x1, ty_Char)
new_gt(x0, x1, app(ty_Maybe, x2))
new_lt1(x0, x1)
new_esEs9(Neg(Zero), Neg(Zero))
new_lt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt0(Char(x0), Char(x1))
new_gt0(Neg(Zero), Neg(Succ(x0)))
new_esEs5(Succ(x0), Succ(x1))
new_esEs9(Neg(Zero), Pos(Zero))
new_esEs9(Pos(Zero), Neg(Zero))
new_esEs2
new_gt(x0, x1, ty_Double)
new_esEs1(Zero, Succ(x0))
new_esEs9(Neg(Succ(x0)), Neg(x1))
new_esEs9(Pos(Zero), Pos(Succ(x0)))
new_gt0(Neg(Zero), Neg(Zero))
new_esEs9(Pos(Succ(x0)), Pos(x1))
new_esEs9(Neg(Zero), Neg(Succ(x0)))
new_gt(Char(x0), Char(x1), ty_Char)
new_gt0(Neg(Succ(x0)), Pos(x1))
new_gt0(Pos(Succ(x0)), Neg(x1))
new_lt(x0, x1, ty_Double)
new_esEs1(Succ(x0), Succ(x1))
new_gt0(Pos(Zero), Pos(Zero))
new_gt(x0, x1, app(ty_[], x2))
new_gt(x0, x1, app(app(ty_Either, x2), x3))
new_lt(x0, x1, ty_Ordering)
new_lt(x0, x1, app(ty_Maybe, x2))
new_gt(x0, x1, ty_Integer)
new_esEs5(Zero, Zero)
new_gt0(Pos(Zero), Neg(Succ(x0)))
new_gt0(Pos(Zero), Pos(Succ(x0)))
new_gt0(Neg(Zero), Pos(Succ(x0)))
new_lt(x0, x1, app(app(ty_Either, x2), x3))
new_lt(x0, x1, ty_Int)
new_esEs1(Succ(x0), Zero)
new_esEs9(Pos(Zero), Pos(Zero))
new_lt(x0, x1, app(app(ty_@2, x2), x3))
new_gt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8
new_gt(x0, x1, ty_Ordering)
new_esEs1(Zero, Zero)
new_lt(x0, x1, ty_Integer)
new_gt0(Neg(Succ(x0)), Neg(x1))
new_lt(x0, x1, app(ty_[], x2))
new_esEs5(Zero, Succ(x0))
new_gt(x0, x1, app(ty_Ratio, x2))
new_esEs6
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, xux2792, Branch(xux27930, xux27931, xux27932, xux27933, xux27934), xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch3MkVBalBranch2(xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs10(new_sizeFM(Branch(xux2850, xux2851, xux2852, xux2853, xux2854), h, ba), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba) → new_mkVBalBranch3MkVBalBranch2(xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs10(new_sizeFM(Branch(xux2850, xux2851, xux2852, xux2853, xux2854), h, ba), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch4(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux2793, xux2794, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Zero), xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch12(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch4(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch1(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux286, xux287, True, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch10(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch1(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, h, ba)
new_mkVBalBranch1(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux2793, xux2794, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Zero), xux2793, xux2794, h, ba)
new_mkVBalBranch3(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux27930, xux27931, xux27932, xux27933, xux27934, h, ba) → new_mkVBalBranch3MkVBalBranch2(xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs10(new_sizeFM(Branch(xux2850, xux2851, xux2852, xux2853, xux2854), h, ba), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, Neg(Zero), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, h, ba) → new_mkVBalBranch3MkVBalBranch12(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs14(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, xux2792, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux2793, h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, h, ba) → new_mkVBalBranch3MkVBalBranch1(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs11(new_primPlusNat0(new_primMulNat(xux279200), Succ(xux279200)), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch3MkVBalBranch12(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux286, xux287, True, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Zero), xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch10(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux286, xux287, True, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Zero), xux2793, xux2794, h, ba)
new_mkVBalBranch2(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux279200, xux2793, xux2794, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, h, ba)
new_mkVBalBranch0(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux279200, xux2793, xux2794, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch1(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch0(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch11(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch2(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, h, ba) → new_mkVBalBranch3MkVBalBranch11(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs13(new_primPlusNat0(new_primMulNat(xux279200), Succ(xux279200)), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, Pos(Zero), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, h, ba) → new_mkVBalBranch3MkVBalBranch10(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs12(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch11(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux286, xux287, True, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, h, ba)
new_esEs18(xux6090, Neg(xux520)) → new_esEs2
new_esEs15(Succ(xux7490), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs18(xux7490, new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba))
new_esEs17(xux6100, Pos(xux520)) → new_esEs3
new_esEs18(xux6090, Pos(xux520)) → new_esEs1(Succ(xux6090), xux520)
new_esEs12(Neg(Succ(xux5200))) → new_esEs2
new_esEs16(Zero, xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs14(new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba))
new_esEs12(Pos(Zero)) → new_esEs4
new_esEs15(Zero, xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs12(new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba))
new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → xux2852
new_primPlusNat0(Succ(xux2100), Succ(xux160)) → Succ(Succ(new_primPlusNat0(xux2100, xux160)))
new_esEs13(Succ(xux6360), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs17(xux6360, new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba))
new_esEs4 → False
new_esEs14(Pos(Succ(xux5200))) → new_esEs3
new_esEs11(Zero, xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs12(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba))
new_esEs10(Neg(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs16(new_primMulNat0(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba)
new_esEs11(Succ(xux6320), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs18(xux6320, new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba))
new_esEs1(Zero, Zero) → new_esEs4
new_esEs14(Neg(Succ(xux5200))) → new_esEs1(Succ(xux5200), Zero)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs1(Succ(xux286000), Zero) → new_esEs2
new_esEs3 → True
new_primMulNat1(xux6200) → new_primPlusNat0(Zero, Succ(xux6200))
new_esEs14(Pos(Zero)) → new_esEs4
new_esEs16(Succ(xux7510), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs17(xux7510, new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba))
new_primMulNat0(Zero) → Zero
new_sizeFM(EmptyFM, bb, bc) → Pos(Zero)
new_esEs13(Zero, xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs14(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba))
new_esEs12(Neg(Zero)) → new_esEs4
new_esEs17(xux6100, Neg(xux520)) → new_esEs1(xux520, Succ(xux6100))
new_primPlusNat0(Zero, Succ(xux160)) → Succ(xux160)
new_primPlusNat0(Succ(xux2100), Zero) → Succ(xux2100)
new_esEs1(Succ(xux286000), Succ(xux281000)) → new_esEs1(xux286000, xux281000)
new_primMulNat(xux6200) → new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(xux6200), Succ(xux6200)), Succ(xux6200)), Succ(xux6200))
new_esEs2 → False
new_primMulNat0(Succ(xux74400)) → new_primPlusNat0(new_primMulNat(xux74400), Succ(xux74400))
new_esEs14(Neg(Zero)) → new_esEs4
new_esEs12(Pos(Succ(xux5200))) → new_esEs1(Zero, Succ(xux5200))
new_sizeFM(Branch(xux7310, xux7311, xux7312, xux7313, xux7314), bb, bc) → xux7312
new_esEs1(Zero, Succ(xux281000)) → new_esEs3
new_esEs10(Pos(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs15(new_primMulNat0(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba)
new_esEs12(Pos(Zero))
new_esEs18(x0, Pos(x1))
new_esEs10(Neg(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs3
new_esEs12(Pos(Succ(x0)))
new_sizeFM(EmptyFM, x0, x1)
new_esEs17(x0, Neg(x1))
new_primPlusNat0(Succ(x0), Zero)
new_sizeFM0(x0, x1, x2, x3, x4, x5, x6)
new_esEs11(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs1(Succ(x0), Succ(x1))
new_primMulNat(x0)
new_esEs4
new_esEs14(Neg(Succ(x0)))
new_esEs16(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_primMulNat0(Zero)
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_esEs17(x0, Pos(x1))
new_esEs13(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs13(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs1(Succ(x0), Zero)
new_esEs12(Neg(Succ(x0)))
new_primMulNat1(x0)
new_esEs14(Pos(Zero))
new_esEs18(x0, Neg(x1))
new_esEs10(Pos(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs1(Zero, Zero)
new_primMulNat0(Succ(x0))
new_esEs11(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_primPlusNat0(Zero, Zero)
new_esEs15(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs14(Neg(Zero))
new_esEs2
new_primPlusNat0(Zero, Succ(x0))
new_esEs1(Zero, Succ(x0))
new_esEs15(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs16(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs14(Pos(Succ(x0)))
new_esEs12(Neg(Zero))
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, xux2792, Branch(xux27930, xux27931, xux27932, xux27933, xux27934), xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch3MkVBalBranch2(xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs10(new_sizeFM(Branch(xux2850, xux2851, xux2852, xux2853, xux2854), h, ba), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba) → new_mkVBalBranch3MkVBalBranch2(xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs10(new_sizeFM(Branch(xux2850, xux2851, xux2852, xux2853, xux2854), h, ba), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch4(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux2793, xux2794, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Zero), xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch12(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch4(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch1(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux286, xux287, True, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch10(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch1(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, h, ba)
new_mkVBalBranch1(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux2793, xux2794, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Zero), xux2793, xux2794, h, ba)
new_mkVBalBranch3(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux27930, xux27931, xux27932, xux27933, xux27934, h, ba) → new_mkVBalBranch3MkVBalBranch2(xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs10(new_sizeFM(Branch(xux2850, xux2851, xux2852, xux2853, xux2854), h, ba), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, Neg(Zero), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, h, ba) → new_mkVBalBranch3MkVBalBranch12(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs14(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, xux2792, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux2793, h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, h, ba) → new_mkVBalBranch3MkVBalBranch1(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs11(new_primPlusNat0(new_primMulNat(xux279200), Succ(xux279200)), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch3MkVBalBranch12(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux286, xux287, True, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Zero), xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch10(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux286, xux287, True, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Zero), xux2793, xux2794, h, ba)
new_mkVBalBranch2(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux279200, xux2793, xux2794, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, h, ba)
new_mkVBalBranch0(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux279200, xux2793, xux2794, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch1(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch0(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch11(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, h, ba) → new_mkVBalBranch2(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, h, ba) → new_mkVBalBranch3MkVBalBranch11(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs13(new_primPlusNat0(new_primMulNat(xux279200), Succ(xux279200)), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba), h, ba)
new_mkVBalBranch3MkVBalBranch2(xux2790, xux2791, Pos(Zero), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, h, ba) → new_mkVBalBranch3MkVBalBranch10(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs12(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch11(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux286, xux287, True, h, ba) → new_mkVBalBranch3(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, h, ba)
new_primMulNat(xux6200) → new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(xux6200), Succ(xux6200)), Succ(xux6200)), Succ(xux6200))
new_primPlusNat0(Succ(xux2100), Succ(xux160)) → Succ(Succ(new_primPlusNat0(xux2100, xux160)))
new_primPlusNat0(Zero, Succ(xux160)) → Succ(xux160)
new_esEs13(Succ(xux6360), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs17(xux6360, new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba))
new_esEs13(Zero, xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs14(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba))
new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → xux2852
new_esEs14(Pos(Succ(xux5200))) → new_esEs3
new_esEs14(Neg(Succ(xux5200))) → new_esEs1(Succ(xux5200), Zero)
new_esEs14(Pos(Zero)) → new_esEs4
new_esEs14(Neg(Zero)) → new_esEs4
new_esEs4 → False
new_esEs1(Succ(xux286000), Zero) → new_esEs2
new_esEs2 → False
new_esEs3 → True
new_esEs17(xux6100, Pos(xux520)) → new_esEs3
new_esEs17(xux6100, Neg(xux520)) → new_esEs1(xux520, Succ(xux6100))
new_esEs1(Succ(xux286000), Succ(xux281000)) → new_esEs1(xux286000, xux281000)
new_esEs1(Zero, Succ(xux281000)) → new_esEs3
new_esEs1(Zero, Zero) → new_esEs4
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(xux2100), Zero) → Succ(xux2100)
new_primMulNat1(xux6200) → new_primPlusNat0(Zero, Succ(xux6200))
new_sizeFM(Branch(xux7310, xux7311, xux7312, xux7313, xux7314), bb, bc) → xux7312
new_esEs10(Neg(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs16(new_primMulNat0(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba)
new_esEs10(Pos(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs15(new_primMulNat0(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba)
new_primMulNat0(Zero) → Zero
new_primMulNat0(Succ(xux74400)) → new_primPlusNat0(new_primMulNat(xux74400), Succ(xux74400))
new_esEs15(Succ(xux7490), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs18(xux7490, new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba))
new_esEs15(Zero, xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs12(new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba))
new_esEs12(Neg(Succ(xux5200))) → new_esEs2
new_esEs12(Pos(Zero)) → new_esEs4
new_esEs12(Neg(Zero)) → new_esEs4
new_esEs12(Pos(Succ(xux5200))) → new_esEs1(Zero, Succ(xux5200))
new_esEs18(xux6090, Neg(xux520)) → new_esEs2
new_esEs18(xux6090, Pos(xux520)) → new_esEs1(Succ(xux6090), xux520)
new_esEs16(Zero, xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs14(new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba))
new_esEs16(Succ(xux7510), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs17(xux7510, new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), h, ba))
new_esEs11(Zero, xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs12(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba))
new_esEs11(Succ(xux6320), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, h, ba) → new_esEs18(xux6320, new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, h, ba))
new_esEs12(Pos(Zero))
new_esEs18(x0, Pos(x1))
new_esEs10(Neg(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs3
new_esEs12(Pos(Succ(x0)))
new_sizeFM(EmptyFM, x0, x1)
new_esEs17(x0, Neg(x1))
new_primPlusNat0(Succ(x0), Zero)
new_sizeFM0(x0, x1, x2, x3, x4, x5, x6)
new_esEs11(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs1(Succ(x0), Succ(x1))
new_primMulNat(x0)
new_esEs4
new_esEs14(Neg(Succ(x0)))
new_esEs16(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_primMulNat0(Zero)
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_esEs17(x0, Pos(x1))
new_esEs13(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs13(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs1(Succ(x0), Zero)
new_esEs12(Neg(Succ(x0)))
new_primMulNat1(x0)
new_esEs14(Pos(Zero))
new_esEs18(x0, Neg(x1))
new_esEs10(Pos(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs1(Zero, Zero)
new_primMulNat0(Succ(x0))
new_esEs11(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_primPlusNat0(Zero, Zero)
new_esEs15(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs14(Neg(Zero))
new_esEs2
new_primPlusNat0(Zero, Succ(x0))
new_esEs1(Zero, Succ(x0))
new_esEs15(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs16(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs14(Pos(Succ(x0)))
new_esEs12(Neg(Zero))
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
new_splitGT1(xux528, xux529, xux530, xux531, xux532, xux533, True, bb) → new_splitGT(xux531, xux533, bb)
new_splitGT3(Char(Zero), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Char(Succ(xux4000)), h) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), h)
new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, Zero, Succ(xux2010), ba) → new_splitGT1(xux194, xux195, xux196, xux197, xux198, xux199, new_esEs1(Succ(xux199), Succ(xux194)), ba)
new_splitGT3(Char(Succ(xux3000)), xux31, xux32, xux33, xux34, Char(Succ(xux4000)), h) → new_splitGT2(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, h)
new_splitGT3(Char(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Char(Zero), h) → new_splitGT3(xux330, xux331, xux332, xux333, xux334, Char(Zero), h)
new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, Zero, Zero, ba) → new_splitGT20(xux194, xux195, xux196, xux197, xux198, xux199, ba)
new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, Succ(xux2000), Succ(xux2010), ba) → new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, xux2000, xux2010, ba)
new_splitGT(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, h) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), h)
new_splitGT20(xux194, xux195, xux196, xux197, xux198, xux199, ba) → new_splitGT1(xux194, xux195, xux196, xux197, xux198, xux199, new_esEs1(Succ(xux199), Succ(xux194)), ba)
new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, Succ(xux2000), Zero, ba) → new_splitGT(xux198, xux199, ba)
new_esEs1(Zero, Zero) → new_esEs4
new_esEs1(Succ(xux286000), Zero) → new_esEs2
new_esEs3 → True
new_esEs1(Succ(xux286000), Succ(xux281000)) → new_esEs1(xux286000, xux281000)
new_esEs2 → False
new_esEs4 → False
new_esEs1(Zero, Succ(xux281000)) → new_esEs3
new_esEs1(Succ(x0), Succ(x1))
new_esEs1(Zero, Zero)
new_esEs3
new_esEs1(Succ(x0), Zero)
new_esEs4
new_esEs2
new_esEs1(Zero, Succ(x0))
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
new_splitGT3(Char(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Char(Zero), h) → new_splitGT3(xux330, xux331, xux332, xux333, xux334, Char(Zero), h)
new_esEs1(Zero, Zero) → new_esEs4
new_esEs1(Succ(xux286000), Zero) → new_esEs2
new_esEs3 → True
new_esEs1(Succ(xux286000), Succ(xux281000)) → new_esEs1(xux286000, xux281000)
new_esEs2 → False
new_esEs4 → False
new_esEs1(Zero, Succ(xux281000)) → new_esEs3
new_esEs1(Succ(x0), Succ(x1))
new_esEs1(Zero, Zero)
new_esEs3
new_esEs1(Succ(x0), Zero)
new_esEs4
new_esEs2
new_esEs1(Zero, Succ(x0))
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
new_splitGT3(Char(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Char(Zero), h) → new_splitGT3(xux330, xux331, xux332, xux333, xux334, Char(Zero), h)
new_esEs1(Succ(x0), Succ(x1))
new_esEs1(Zero, Zero)
new_esEs3
new_esEs1(Succ(x0), Zero)
new_esEs4
new_esEs2
new_esEs1(Zero, Succ(x0))
new_esEs1(Succ(x0), Succ(x1))
new_esEs1(Zero, Zero)
new_esEs3
new_esEs1(Succ(x0), Zero)
new_esEs4
new_esEs2
new_esEs1(Zero, Succ(x0))
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
new_splitGT3(Char(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Char(Zero), h) → new_splitGT3(xux330, xux331, xux332, xux333, xux334, Char(Zero), h)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
new_splitGT1(xux528, xux529, xux530, xux531, xux532, xux533, True, bb) → new_splitGT(xux531, xux533, bb)
new_splitGT3(Char(Zero), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Char(Succ(xux4000)), h) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), h)
new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, Zero, Succ(xux2010), ba) → new_splitGT1(xux194, xux195, xux196, xux197, xux198, xux199, new_esEs1(Succ(xux199), Succ(xux194)), ba)
new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, Zero, Zero, ba) → new_splitGT20(xux194, xux195, xux196, xux197, xux198, xux199, ba)
new_splitGT3(Char(Succ(xux3000)), xux31, xux32, xux33, xux34, Char(Succ(xux4000)), h) → new_splitGT2(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, h)
new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, Succ(xux2000), Succ(xux2010), ba) → new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, xux2000, xux2010, ba)
new_splitGT20(xux194, xux195, xux196, xux197, xux198, xux199, ba) → new_splitGT1(xux194, xux195, xux196, xux197, xux198, xux199, new_esEs1(Succ(xux199), Succ(xux194)), ba)
new_splitGT(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, h) → new_splitGT3(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), h)
new_splitGT2(xux194, xux195, xux196, xux197, xux198, xux199, Succ(xux2000), Zero, ba) → new_splitGT(xux198, xux199, ba)
new_esEs1(Zero, Zero) → new_esEs4
new_esEs1(Succ(xux286000), Zero) → new_esEs2
new_esEs3 → True
new_esEs1(Succ(xux286000), Succ(xux281000)) → new_esEs1(xux286000, xux281000)
new_esEs2 → False
new_esEs4 → False
new_esEs1(Zero, Succ(xux281000)) → new_esEs3
new_esEs1(Succ(x0), Succ(x1))
new_esEs1(Zero, Zero)
new_esEs3
new_esEs1(Succ(x0), Zero)
new_esEs4
new_esEs2
new_esEs1(Zero, Succ(x0))
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
new_splitLT3(Char(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Char(Zero), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Char(Zero), ba)
new_splitLT20(xux185, xux186, xux187, xux188, xux189, xux190, bb) → new_splitLT1(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux190), Succ(xux185), bb)
new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux1910), Succ(xux1920), bb) → new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, xux1910, xux1920, bb)
new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, Zero, Zero, bb) → new_splitLT20(xux185, xux186, xux187, xux188, xux189, xux190, bb)
new_splitLT3(Char(Succ(xux3000)), xux31, xux32, xux33, xux34, Char(Succ(xux4000)), ba) → new_splitLT2(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, ba)
new_splitLT3(Char(Zero), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Char(Succ(xux4000)), ba) → new_splitLT3(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), ba)
new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux1910), Zero, bb) → new_splitLT1(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux190), Succ(xux185), bb)
new_splitLT(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, ba) → new_splitLT3(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), ba)
new_splitLT1(xux519, xux520, xux521, xux522, xux523, xux524, Succ(xux5250), Zero, h) → new_splitLT(xux523, xux524, h)
new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, Zero, Succ(xux1920), bb) → new_splitLT(xux188, xux190, bb)
new_splitLT1(xux519, xux520, xux521, xux522, xux523, xux524, Succ(xux5250), Succ(xux5260), h) → new_splitLT1(xux519, xux520, xux521, xux522, xux523, xux524, xux5250, xux5260, h)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
new_splitLT3(Char(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Char(Zero), ba) → new_splitLT3(xux330, xux331, xux332, xux333, xux334, Char(Zero), ba)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
new_splitLT20(xux185, xux186, xux187, xux188, xux189, xux190, bb) → new_splitLT1(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux190), Succ(xux185), bb)
new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux1910), Succ(xux1920), bb) → new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, xux1910, xux1920, bb)
new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, Zero, Zero, bb) → new_splitLT20(xux185, xux186, xux187, xux188, xux189, xux190, bb)
new_splitLT3(Char(Succ(xux3000)), xux31, xux32, xux33, xux34, Char(Succ(xux4000)), ba) → new_splitLT2(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, ba)
new_splitLT3(Char(Zero), xux31, xux32, xux33, Branch(xux340, xux341, xux342, xux343, xux344), Char(Succ(xux4000)), ba) → new_splitLT3(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), ba)
new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux1910), Zero, bb) → new_splitLT1(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux190), Succ(xux185), bb)
new_splitLT(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, ba) → new_splitLT3(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), ba)
new_splitLT1(xux519, xux520, xux521, xux522, xux523, xux524, Succ(xux5250), Zero, h) → new_splitLT(xux523, xux524, h)
new_splitLT2(xux185, xux186, xux187, xux188, xux189, xux190, Zero, Succ(xux1920), bb) → new_splitLT(xux188, xux190, bb)
new_splitLT1(xux519, xux520, xux521, xux522, xux523, xux524, Succ(xux5250), Succ(xux5260), h) → new_splitLT1(xux519, xux520, xux521, xux522, xux523, xux524, xux5250, xux5260, h)
From the DPs we obtained the following set of size-change graphs:
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ NumRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
new_plusFM(Branch(xux30, xux31, xux32, xux33, xux34), Branch(xux40, xux41, xux42, xux43, xux44), h) → new_plusFM(new_splitGT30(xux30, xux31, xux32, xux33, xux34, xux40, h), xux44, h)
new_plusFM(Branch(xux30, xux31, xux32, xux33, xux34), Branch(xux40, xux41, xux42, xux43, xux44), h) → new_plusFM(new_splitLT30(xux30, xux31, xux32, xux33, xux34, xux40, h), xux43, h)
new_lt(xux652, xux6500, ty_Float) → error([])
new_addToFM_C0(Branch(xux50, xux51, xux52, xux53, xux54), xux40, xux41, h) → new_addToFM_C20(xux50, xux51, xux52, xux53, xux54, xux40, xux41, new_lt0(xux40, xux50), ty_Char, h)
new_esEs8 → False
new_gt(xux652, xux647, ty_Integer) → error([])
new_mkBranch3(xux675, xux676, xux677, xux678, xux679, xux680, xux681, xux682, xux683, xux684, xux685, xux686, xux687, ef, eg) → Branch(xux676, xux677, new_primPlusInt(new_ps(Branch(xux678, xux679, xux680, xux681, xux682), Branch(xux683, xux684, Pos(Succ(xux685)), xux686, xux687), xux676, ef, eg), new_mkBranchRight_size(Branch(xux678, xux679, xux680, xux681, xux682), Branch(xux683, xux684, Pos(Succ(xux685)), xux686, xux687), xux676, ef, eg)), Branch(xux678, xux679, xux680, xux681, xux682), Branch(xux683, xux684, Pos(Succ(xux685)), xux686, xux687))
new_mkVBalBranch3MkVBalBranch13(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, ba, bb) → new_mkBranch1(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))), xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb)
new_splitLT22(xux185, xux186, xux187, xux188, xux189, xux190, bf) → new_splitLT10(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux190), Succ(xux185), bf)
new_esEs9(Pos(Zero), Neg(Succ(xux650000))) → new_esEs2
new_mkVBalBranch10(xux286, xux287, EmptyFM, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb) → new_addToFM(xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, xux286, xux287, ba, bb)
new_splitLT21(xux185, xux186, xux187, xux188, xux189, xux190, Zero, Succ(xux1920), bf) → new_splitLT0(xux188, xux190, bf)
new_mkVBalBranch9(xux286, xux287, EmptyFM, xux2790, xux2791, xux2793, xux2794, ba, bb) → new_addToFM(xux2790, xux2791, Pos(Zero), xux2793, xux2794, xux286, xux287, ba, bb)
new_mkVBalBranch7(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux2793, xux2794, ba, bb) → new_mkVBalBranch30(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Zero), xux2793, xux2794, ba, bb)
new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → xux2852
new_esEs9(Pos(Zero), Pos(Zero)) → new_esEs4
new_mkBalBranch6Size_l(xux747, xux665, xux666, xux668, bd, be) → new_sizeFM(xux668, bd, be)
new_esEs19(Succ(xux7600)) → new_esEs3
new_esEs14(Pos(Succ(xux5200))) → new_esEs3
new_splitLT21(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux1910), Zero, bf) → new_splitLT22(xux185, xux186, xux187, xux188, xux189, xux190, bf)
new_primPlusInt(Neg(xux7740), Pos(xux7730)) → new_primMinusNat0(xux7730, xux7740)
new_primPlusInt(Pos(xux7740), Neg(xux7730)) → new_primMinusNat0(xux7740, xux7730)
new_mkBalBranch6MkBalBranch3(xux731, xux665, xux666, Branch(xux6680, xux6681, xux6682, xux6683, xux6684), xux730, True, bd, be) → new_mkBalBranch6MkBalBranch11(xux731, xux665, xux666, xux6680, xux6681, xux6682, xux6683, xux6684, xux730, new_lt1(new_sizeFM(xux6684, bd, be), new_sr0(new_sizeFM(xux6683, bd, be))), bd, be)
new_esEs3 → True
new_mkBalBranch6MkBalBranch5(xux731, xux665, xux666, xux668, xux730, True, bd, be) → new_mkBranchResult(xux665, xux666, xux668, xux730, bd, be)
new_splitLT30(Char(Succ(xux3000)), xux31, xux32, xux33, xux34, Char(Succ(xux4000)), h) → new_splitLT21(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, h)
new_lt0(Char(xux400), Char(xux500)) → new_esEs1(xux400, xux500)
new_esEs9(Neg(Zero), Pos(Succ(xux650000))) → new_esEs3
new_gt0(Pos(Zero), Neg(Zero)) → new_esEs8
new_gt0(Neg(Zero), Pos(Zero)) → new_esEs8
new_addToFM_C3(EmptyFM, xux652, xux653, ca, cb) → Branch(xux652, xux653, Pos(Succ(Zero)), new_emptyFM0(ca, cb), new_emptyFM0(ca, cb))
new_addToFM_C20(xux647, xux648, xux649, xux650, xux651, xux652, xux653, False, ca, cb) → new_addToFM_C10(xux647, xux648, xux649, xux650, xux651, xux652, xux653, new_gt(xux652, xux647, ca), ca, cb)
new_addToFM_C3(Branch(xux6500, xux6501, xux6502, xux6503, xux6504), xux652, xux653, ca, cb) → new_addToFM_C20(xux6500, xux6501, xux6502, xux6503, xux6504, xux652, xux653, new_lt(xux652, xux6500, ca), ca, cb)
new_sr(Pos(xux7580)) → Pos(new_primMulNat0(xux7580))
new_esEs1(Succ(xux286000), Succ(xux281000)) → new_esEs1(xux286000, xux281000)
new_esEs9(Neg(Zero), Neg(Zero)) → new_esEs4
new_addToFM(xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, ba, bb) → new_addToFM_C3(Branch(xux2850, xux2851, xux2852, xux2853, xux2854), xux286, xux287, ba, bb)
new_gt(xux652, xux647, app(ty_Ratio, cc)) → error([])
new_lt(xux652, xux6500, app(ty_Ratio, cc)) → error([])
new_mkVBalBranch8(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, EmptyFM, ba, bb) → new_addToFM(xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, ba, bb)
new_lt(xux652, xux6500, ty_Ordering) → error([])
new_esEs5(Succ(xux65200), Succ(xux64700)) → new_esEs5(xux65200, xux64700)
new_mkBranch4(xux702, xux703, xux704, xux705, xux706, xux707, xux708, xux709, xux710, xux711, xux712, xux713, xux714, dh, ea) → Branch(xux703, xux704, new_primPlusInt(new_ps(Branch(xux705, xux706, xux707, xux708, xux709), Branch(xux710, xux711, Neg(Succ(xux712)), xux713, xux714), xux703, dh, ea), new_mkBranchRight_size(Branch(xux705, xux706, xux707, xux708, xux709), Branch(xux710, xux711, Neg(Succ(xux712)), xux713, xux714), xux703, dh, ea)), Branch(xux705, xux706, xux707, xux708, xux709), Branch(xux710, xux711, Neg(Succ(xux712)), xux713, xux714))
new_esEs22(Succ(xux75600), Succ(xux75300)) → new_esEs9(new_primMinusNat0(xux75600, xux75300), Pos(Succ(Succ(Zero))))
new_esEs22(Zero, Succ(xux75300)) → new_esEs9(Neg(Succ(xux75300)), Pos(Succ(Succ(Zero))))
new_lt(xux652, xux6500, ty_Integer) → error([])
new_sr(Neg(xux7580)) → Neg(new_primMulNat0(xux7580))
new_esEs12(Pos(Zero)) → new_esEs4
new_mkVBalBranch6(xux286, xux287, EmptyFM, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb) → new_addToFM(xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, xux286, xux287, ba, bb)
new_gt0(Pos(Succ(xux65200)), Pos(xux6470)) → new_esEs5(Succ(xux65200), xux6470)
new_primMulNat2(Succ(xux76600)) → new_primPlusNat0(new_primMulNat1(xux76600), Succ(xux76600))
new_mkBranchRight_size(xux668, xux730, xux665, bd, be) → new_sizeFM(xux730, bd, be)
new_lt(xux652, xux6500, ty_Bool) → error([])
new_esEs14(Neg(Succ(xux5200))) → new_esEs1(Succ(xux5200), Zero)
new_gt0(Neg(Succ(xux65200)), Neg(xux6470)) → new_esEs5(xux6470, Succ(xux65200))
new_mkVBalBranch3MkVBalBranch20(xux2790, xux2791, Pos(Zero), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, ba, bb) → new_mkVBalBranch3MkVBalBranch16(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs12(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb)), ba, bb)
new_esEs9(Neg(Succ(xux65200)), Neg(xux65000)) → new_esEs1(xux65000, Succ(xux65200))
new_mkBalBranch6MkBalBranch4(xux731, xux665, xux666, xux668, xux730, False, bd, be) → new_mkBalBranch6MkBalBranch3(xux731, xux665, xux666, xux668, xux730, new_gt0(new_mkBalBranch6Size_l(xux731, xux665, xux666, xux668, bd, be), new_sr(new_mkBalBranch6Size_r(xux731, xux665, xux666, xux668, bd, be))), bd, be)
new_gt0(Pos(Zero), Neg(Succ(xux64700))) → new_esEs6
new_mkVBalBranch3MkVBalBranch13(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, ba, bb) → new_mkBalBranch6MkBalBranch5(new_mkVBalBranch7(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb), xux2850, xux2851, xux2853, new_mkVBalBranch7(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb), new_lt2(new_mkVBalBranch7(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb), xux2850, xux2851, xux2853, new_mkVBalBranch7(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb), ba, bb), ba, bb)
new_mkBalBranch6Size_r(xux731, xux665, xux666, xux668, bd, be) → new_sizeFM(xux731, bd, be)
new_mkBalBranch6MkBalBranch01(xux731, xux665, xux666, xux668, xux7300, xux7301, xux7302, xux7303, xux7304, True, bd, be) → new_mkBranchResult(xux7300, xux7301, new_mkBranchResult(xux665, xux666, xux668, xux7303, bd, be), xux7304, bd, be)
new_mkBalBranch6MkBalBranch5(xux731, xux665, xux666, xux668, xux730, False, bd, be) → new_mkBalBranch6MkBalBranch4(xux731, xux665, xux666, xux668, xux730, new_gt0(new_mkBalBranch6Size_r(xux731, xux665, xux666, xux668, bd, be), new_sr(new_mkBalBranch6Size_l(xux731, xux665, xux666, xux668, bd, be))), bd, be)
new_esEs9(Pos(Succ(xux65200)), Neg(xux65000)) → new_esEs2
new_gt(xux652, xux647, ty_Int) → new_gt0(xux652, xux647)
new_mkBranch1(xux716, xux717, xux718, xux719, xux720, xux721, xux722, xux723, xux724, xux725, xux726, xux727, ed, ee) → Branch(xux717, xux718, new_primPlusInt(new_ps(Branch(xux719, xux720, xux721, xux722, xux723), Branch(xux724, xux725, Neg(Zero), xux726, xux727), xux717, ed, ee), new_mkBranchRight_size(Branch(xux719, xux720, xux721, xux722, xux723), Branch(xux724, xux725, Neg(Zero), xux726, xux727), xux717, ed, ee)), Branch(xux719, xux720, xux721, xux722, xux723), Branch(xux724, xux725, Neg(Zero), xux726, xux727))
new_mkVBalBranch3MkVBalBranch14(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, ba, bb) → new_mkBalBranch6MkBalBranch5(new_mkVBalBranch6(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb), xux2850, xux2851, xux2853, new_mkVBalBranch6(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb), new_lt2(new_mkVBalBranch6(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb), xux2850, xux2851, xux2853, new_mkVBalBranch6(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb), ba, bb), ba, bb)
new_splitGT4(EmptyFM, h) → new_emptyFM(h)
new_lt(xux652, xux6500, app(app(app(ty_@3, ce), cf), cg)) → error([])
new_gt0(Neg(Zero), Neg(Succ(xux64700))) → new_esEs5(Succ(xux64700), Zero)
new_esEs20(Zero) → new_esEs1(Zero, Succ(Succ(Zero)))
new_splitLT30(Char(Zero), xux31, xux32, xux33, xux34, Char(Zero), h) → xux33
new_sr0(Pos(xux7660)) → Pos(new_primMulNat2(xux7660))
new_mkBalBranch6MkBalBranch4(xux731, xux665, xux666, xux668, EmptyFM, True, bd, be) → error([])
new_gt0(Neg(Zero), Neg(Zero)) → new_esEs8
new_esEs21(Neg(xux7560), Neg(xux7530)) → new_esEs19(new_primPlusNat0(xux7560, xux7530))
new_mkVBalBranch3MkVBalBranch20(xux2790, xux2791, Neg(Zero), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, ba, bb) → new_mkVBalBranch3MkVBalBranch13(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs14(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb)), ba, bb)
new_lt1(xux652, xux6500) → new_esEs9(xux652, xux6500)
new_splitGT30(Char(Zero), xux31, xux32, xux33, xux34, Char(Zero), h) → xux34
new_primPlusNat0(Zero, Zero) → Zero
new_esEs9(Neg(Zero), Neg(Succ(xux650000))) → new_esEs1(Succ(xux650000), Zero)
new_splitGT0(EmptyFM, xux4000, h) → new_emptyFM(h)
new_primPlusInt(Neg(xux7740), Neg(xux7730)) → Neg(new_primPlusNat0(xux7740, xux7730))
new_lt(xux652, xux6500, app(app(ty_Either, da), db)) → error([])
new_esEs16(Succ(xux7510), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs17(xux7510, new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), ba, bb))
new_lt(xux652, xux6500, app(app(ty_@2, dd), de)) → error([])
new_mkBranch2(xux689, xux690, xux691, xux692, xux693, xux694, xux695, xux696, xux697, xux698, xux699, xux700, df, dg) → Branch(xux690, xux691, new_primPlusInt(new_ps(Branch(xux692, xux693, xux694, xux695, xux696), Branch(xux697, xux698, Pos(Zero), xux699, xux700), xux690, df, dg), new_mkBranchRight_size(Branch(xux692, xux693, xux694, xux695, xux696), Branch(xux697, xux698, Pos(Zero), xux699, xux700), xux690, df, dg)), Branch(xux692, xux693, xux694, xux695, xux696), Branch(xux697, xux698, Pos(Zero), xux699, xux700))
new_primMulNat0(Zero) → Zero
new_mkVBalBranch3MkVBalBranch15(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, ba, bb) → new_mkBranch4(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))), xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb)
new_gt(xux652, xux647, app(ty_[], dc)) → error([])
new_mkVBalBranch5(xux40, xux41, Branch(xux60, xux61, xux62, xux63, xux64), Branch(xux50, xux51, xux52, xux53, xux54), h) → new_mkVBalBranch3MkVBalBranch20(xux50, xux51, xux52, xux53, xux54, xux60, xux61, xux62, xux63, xux64, xux40, xux41, new_esEs10(new_sizeFM0(xux60, xux61, xux62, xux63, xux64, ty_Char, h), xux50, xux51, xux52, xux53, xux54, xux60, xux61, xux62, xux63, xux64, ty_Char, h), ty_Char, h)
new_sizeFM(Branch(xux7310, xux7311, xux7312, xux7313, xux7314), bd, be) → xux7312
new_esEs10(Pos(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs15(new_primMulNat0(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb)
new_splitGT21(xux194, xux195, xux196, xux197, xux198, xux199, Succ(xux2000), Succ(xux2010), bg) → new_splitGT21(xux194, xux195, xux196, xux197, xux198, xux199, xux2000, xux2010, bg)
new_mkVBalBranch3MkVBalBranch16(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, ba, bb) → new_mkBranch2(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))), xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb)
new_mkBalBranch6MkBalBranch3(xux731, xux665, xux666, EmptyFM, xux730, True, bd, be) → error([])
new_esEs18(xux6090, Neg(xux520)) → new_esEs2
new_gt(xux652, xux647, ty_Bool) → error([])
new_primMinusNat0(Zero, Zero) → Pos(Zero)
new_esEs12(Neg(Succ(xux5200))) → new_esEs2
new_esEs21(Pos(xux7560), Pos(xux7530)) → new_esEs20(new_primPlusNat0(xux7560, xux7530))
new_esEs4 → False
new_lt2(xux747, xux665, xux666, xux668, xux746, bd, be) → new_esEs21(new_mkBalBranch6Size_l(xux747, xux665, xux666, xux668, bd, be), new_mkBalBranch6Size_r(xux746, xux665, xux666, xux668, bd, be))
new_splitLT0(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, h) → new_splitLT30(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), h)
new_esEs1(Zero, Zero) → new_esEs4
new_esEs1(Succ(xux286000), Zero) → new_esEs2
new_gt(xux652, xux647, app(app(ty_@2, dd), de)) → error([])
new_mkVBalBranch3MkVBalBranch15(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, ba, bb) → new_mkBalBranch6MkBalBranch5(new_mkVBalBranch10(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb), xux2850, xux2851, xux2853, new_mkVBalBranch10(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb), new_lt2(new_mkVBalBranch10(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb), xux2850, xux2851, xux2853, new_mkVBalBranch10(xux286, xux287, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb), ba, bb), ba, bb)
new_primPlusInt(Pos(xux7740), Pos(xux7730)) → Pos(new_primPlusNat0(xux7740, xux7730))
new_esEs14(Pos(Zero)) → new_esEs4
new_esEs20(Succ(xux7590)) → new_esEs1(Succ(xux7590), Succ(Succ(Zero)))
new_esEs6 → True
new_esEs12(Neg(Zero)) → new_esEs4
new_splitLT10(xux519, xux520, xux521, xux522, xux523, xux524, Zero, Succ(xux5260), bh) → new_splitLT11(xux519, xux520, xux521, xux522, xux523, xux524, bh)
new_primMulNat(xux6200) → new_primPlusNat0(new_primPlusNat0(new_primPlusNat0(new_primMulNat1(xux6200), Succ(xux6200)), Succ(xux6200)), Succ(xux6200))
new_mkBranch0(xux801, xux802, xux803, xux804, xux805, eb, ec) → new_mkBranchResult(xux802, xux803, xux804, xux805, eb, ec)
new_gt(xux652, xux647, app(app(ty_Either, da), db)) → error([])
new_mkVBalBranch3MkVBalBranch14(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, ba, bb) → new_mkBranch3(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))), xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb)
new_esEs22(Succ(xux75600), Zero) → new_esEs9(Pos(Succ(xux75600)), Pos(Succ(Succ(Zero))))
new_esEs9(Pos(Zero), Pos(Succ(xux650000))) → new_esEs1(Zero, Succ(xux650000))
new_splitGT21(xux194, xux195, xux196, xux197, xux198, xux199, Succ(xux2000), Zero, bg) → new_splitGT0(xux198, xux199, bg)
new_splitLT30(Char(Succ(xux3000)), xux31, xux32, EmptyFM, xux34, Char(Zero), h) → new_emptyFM(h)
new_gt0(Pos(Succ(xux65200)), Neg(xux6470)) → new_esEs6
new_mkVBalBranch5(xux40, xux41, EmptyFM, xux5, h) → new_addToFM0(xux5, xux40, xux41, h)
new_esEs22(Zero, Zero) → new_esEs9(Pos(Zero), Pos(Succ(Succ(Zero))))
new_emptyFM(h) → EmptyFM
new_mkVBalBranch8(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, Branch(xux27930, xux27931, xux27932, xux27933, xux27934), ba, bb) → new_mkVBalBranch30(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux27930, xux27931, xux27932, xux27933, xux27934, ba, bb)
new_mkVBalBranch3MkVBalBranch20(xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, ba, bb) → new_mkVBalBranch3MkVBalBranch15(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs13(new_primPlusNat0(new_primMulNat(xux279200), Succ(xux279200)), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb), ba, bb)
new_mkBalBranch6MkBalBranch3(xux731, xux665, xux666, xux668, xux730, False, bd, be) → new_mkBranchResult(xux665, xux666, xux668, xux730, bd, be)
new_splitGT30(Char(Zero), xux31, xux32, xux33, xux34, Char(Succ(xux4000)), h) → new_splitGT0(xux34, xux4000, h)
new_mkBranchResult(xux665, xux666, xux668, xux730, bd, be) → Branch(xux665, xux666, new_primPlusInt(new_ps(xux668, xux730, xux665, bd, be), new_mkBranchRight_size(xux668, xux730, xux665, bd, be)), xux668, xux730)
new_lt(xux652, xux6500, ty_Int) → new_lt1(xux652, xux6500)
new_gt(Char(xux6520), Char(xux6470), ty_Char) → new_esEs5(xux6520, xux6470)
new_gt(xux652, xux647, ty_Float) → error([])
new_splitLT10(xux519, xux520, xux521, xux522, xux523, xux524, Succ(xux5250), Succ(xux5260), bh) → new_splitLT10(xux519, xux520, xux521, xux522, xux523, xux524, xux5250, xux5260, bh)
new_splitGT21(xux194, xux195, xux196, xux197, xux198, xux199, Zero, Succ(xux2010), bg) → new_splitGT22(xux194, xux195, xux196, xux197, xux198, xux199, bg)
new_gt(xux652, xux647, app(app(app(ty_@3, ce), cf), cg)) → error([])
new_esEs2 → False
new_mkVBalBranch30(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux27930, xux27931, xux27932, xux27933, xux27934, ba, bb) → new_mkVBalBranch3MkVBalBranch20(xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs10(new_sizeFM(Branch(xux2850, xux2851, xux2852, xux2853, xux2854), ba, bb), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb), ba, bb)
new_splitLT10(xux519, xux520, xux521, xux522, xux523, xux524, Zero, Zero, bh) → new_splitLT11(xux519, xux520, xux521, xux522, xux523, xux524, bh)
new_gt(xux652, xux647, ty_@0) → error([])
new_gt(xux652, xux647, ty_Ordering) → error([])
new_mkVBalBranch6(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb) → new_mkVBalBranch30(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, ba, bb)
new_mkBalBranch6MkBalBranch11(xux731, xux665, xux666, xux6680, xux6681, xux6682, xux6683, xux6684, xux730, True, bd, be) → new_mkBranch(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))), xux6680, xux6681, xux6683, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))), xux665, xux666, xux6684, xux730, bd, be)
new_mkVBalBranch5(xux40, xux41, Branch(xux60, xux61, xux62, xux63, xux64), EmptyFM, h) → new_addToFM0(Branch(xux60, xux61, xux62, xux63, xux64), xux40, xux41, h)
new_esEs9(Pos(Zero), Neg(Zero)) → new_esEs4
new_esEs9(Neg(Zero), Pos(Zero)) → new_esEs4
new_splitLT21(xux185, xux186, xux187, xux188, xux189, xux190, Zero, Zero, bf) → new_splitLT22(xux185, xux186, xux187, xux188, xux189, xux190, bf)
new_esEs15(Succ(xux7490), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs18(xux7490, new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), ba, bb))
new_esEs17(xux6100, Pos(xux520)) → new_esEs3
new_esEs18(xux6090, Pos(xux520)) → new_esEs1(Succ(xux6090), xux520)
new_mkBalBranch6MkBalBranch01(xux731, xux665, xux666, xux668, xux7300, xux7301, xux7302, Branch(xux73030, xux73031, xux73032, xux73033, xux73034), xux7304, False, bd, be) → new_mkBranch(Succ(Succ(Succ(Succ(Zero)))), xux73030, xux73031, new_mkBranchResult(xux665, xux666, xux668, xux73033, bd, be), Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))), xux7300, xux7301, xux73034, xux7304, bd, be)
new_esEs15(Zero, xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs12(new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), ba, bb))
new_splitGT4(Branch(xux330, xux331, xux332, xux333, xux334), h) → new_splitGT30(xux330, xux331, xux332, xux333, xux334, Char(Zero), h)
new_addToFM_C10(xux665, xux666, xux667, xux668, xux669, xux670, xux671, True, bd, be) → new_mkBalBranch6MkBalBranch5(new_addToFM_C3(xux669, xux670, xux671, bd, be), xux665, xux666, xux668, new_addToFM_C3(xux669, xux670, xux671, bd, be), new_lt2(new_addToFM_C3(xux669, xux670, xux671, bd, be), xux665, xux666, xux668, new_addToFM_C3(xux669, xux670, xux671, bd, be), bd, be), bd, be)
new_primMinusNat0(Zero, Succ(xux753000)) → Neg(Succ(xux753000))
new_mkVBalBranch3MkVBalBranch16(xux2790, xux2791, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, ba, bb) → new_mkBalBranch6MkBalBranch5(new_mkVBalBranch9(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb), xux2850, xux2851, xux2853, new_mkVBalBranch9(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb), new_lt2(new_mkVBalBranch9(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb), xux2850, xux2851, xux2853, new_mkVBalBranch9(xux286, xux287, xux2854, xux2790, xux2791, xux2793, xux2794, ba, bb), ba, bb), ba, bb)
new_esEs13(Succ(xux6360), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs17(xux6360, new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb))
new_esEs5(Zero, Succ(xux64700)) → new_esEs7
new_splitGT22(xux194, xux195, xux196, xux197, xux198, xux199, bg) → new_splitGT10(xux194, xux195, xux196, xux197, xux198, xux199, new_esEs1(Succ(xux199), Succ(xux194)), bg)
new_esEs11(Succ(xux6320), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs18(xux6320, new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb))
new_splitLT21(xux185, xux186, xux187, xux188, xux189, xux190, Succ(xux1910), Succ(xux1920), bf) → new_splitLT21(xux185, xux186, xux187, xux188, xux189, xux190, xux1910, xux1920, bf)
new_splitGT30(Char(Succ(xux3000)), xux31, xux32, xux33, xux34, Char(Zero), h) → new_mkVBalBranch5(Char(Succ(xux3000)), xux31, new_splitGT4(xux33, h), xux34, h)
new_esEs13(Zero, xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs14(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb))
new_lt(xux652, xux6500, ty_@0) → error([])
new_primMulNat0(Succ(xux74400)) → new_primPlusNat0(new_primMulNat(xux74400), Succ(xux74400))
new_splitGT21(xux194, xux195, xux196, xux197, xux198, xux199, Zero, Zero, bg) → new_splitGT22(xux194, xux195, xux196, xux197, xux198, xux199, bg)
new_esEs1(Zero, Succ(xux281000)) → new_esEs3
new_addToFM_C20(xux647, xux648, xux649, xux650, xux651, xux652, xux653, True, ca, cb) → new_mkBalBranch6MkBalBranch5(xux651, xux647, xux648, new_addToFM_C3(xux650, xux652, xux653, ca, cb), xux651, new_lt2(xux651, xux647, xux648, new_addToFM_C3(xux650, xux652, xux653, ca, cb), xux651, ca, cb), ca, cb)
new_splitLT11(xux519, xux520, xux521, xux522, xux523, xux524, bh) → xux522
new_gt0(Neg(Zero), Pos(Succ(xux64700))) → new_esEs7
new_splitLT30(Char(Zero), xux31, xux32, xux33, xux34, Char(Succ(xux4000)), h) → new_mkVBalBranch5(Char(Zero), xux31, xux33, new_splitLT0(xux34, xux4000, h), h)
new_sr0(Neg(xux7660)) → Neg(new_primMulNat2(xux7660))
new_mkBranch(xux797, xux798, xux799, xux800, xux801, xux802, xux803, xux804, xux805, eb, ec) → new_mkBranchResult(xux798, xux799, xux800, new_mkBranch0(xux801, xux802, xux803, xux804, xux805, eb, ec), eb, ec)
new_esEs5(Succ(xux65200), Zero) → new_esEs6
new_esEs5(Zero, Zero) → new_esEs8
new_gt(xux652, xux647, app(ty_Maybe, cd)) → error([])
new_primPlusNat0(Succ(xux2100), Succ(xux160)) → Succ(Succ(new_primPlusNat0(xux2100, xux160)))
new_mkVBalBranch10(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux279200, xux2793, xux2794, ba, bb) → new_mkVBalBranch30(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Neg(Succ(xux279200)), xux2793, xux2794, ba, bb)
new_mkBalBranch6MkBalBranch4(xux731, xux665, xux666, xux668, Branch(xux7300, xux7301, xux7302, xux7303, xux7304), True, bd, be) → new_mkBalBranch6MkBalBranch01(xux731, xux665, xux666, xux668, xux7300, xux7301, xux7302, xux7303, xux7304, new_lt1(new_sizeFM(xux7303, bd, be), new_sr0(new_sizeFM(xux7304, bd, be))), bd, be)
new_esEs10(Neg(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs16(new_primMulNat0(xux7440), xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb)
new_mkVBalBranch3MkVBalBranch20(xux2790, xux2791, xux2792, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, True, ba, bb) → new_mkBalBranch6MkBalBranch5(xux2794, xux2790, xux2791, new_mkVBalBranch8(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux2793, ba, bb), xux2794, new_lt2(xux2794, xux2790, xux2791, new_mkVBalBranch8(xux286, xux287, xux2850, xux2851, xux2852, xux2853, xux2854, xux2793, ba, bb), xux2794, ba, bb), ba, bb)
new_gt(xux652, xux647, ty_Double) → error([])
new_primMulNat1(xux6200) → new_primPlusNat0(Zero, Succ(xux6200))
new_esEs9(Neg(Succ(xux65200)), Pos(xux65000)) → new_esEs3
new_mkBalBranch6MkBalBranch11(xux731, xux665, xux666, xux6680, xux6681, xux6682, xux6683, Branch(xux66840, xux66841, xux66842, xux66843, xux66844), xux730, False, bd, be) → new_mkBranch(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))), xux66840, xux66841, new_mkBranch0(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))), xux6680, xux6681, xux6683, xux66843, bd, be), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))), xux665, xux666, xux66844, xux730, bd, be)
new_splitGT10(xux528, xux529, xux530, xux531, xux532, xux533, True, bc) → new_mkVBalBranch5(Char(Succ(xux528)), xux529, new_splitGT0(xux531, xux533, bc), xux532, bc)
new_splitLT0(EmptyFM, xux4000, h) → new_emptyFM(h)
new_primMinusNat0(Succ(xux756000), Zero) → Pos(Succ(xux756000))
new_sizeFM(EmptyFM, bd, be) → Pos(Zero)
new_mkVBalBranch7(xux286, xux287, EmptyFM, xux2790, xux2791, xux2793, xux2794, ba, bb) → new_addToFM(xux2790, xux2791, Neg(Zero), xux2793, xux2794, xux286, xux287, ba, bb)
new_esEs9(Pos(Succ(xux65200)), Pos(xux65000)) → new_esEs1(Succ(xux65200), xux65000)
new_esEs17(xux6100, Neg(xux520)) → new_esEs1(xux520, Succ(xux6100))
new_addToFM0(xux5, xux40, xux41, h) → new_addToFM_C0(xux5, xux40, xux41, h)
new_mkVBalBranch9(xux286, xux287, Branch(xux28540, xux28541, xux28542, xux28543, xux28544), xux2790, xux2791, xux2793, xux2794, ba, bb) → new_mkVBalBranch30(xux286, xux287, xux28540, xux28541, xux28542, xux28543, xux28544, xux2790, xux2791, Pos(Zero), xux2793, xux2794, ba, bb)
new_mkBalBranch6MkBalBranch01(xux731, xux665, xux666, xux668, xux7300, xux7301, xux7302, EmptyFM, xux7304, False, bd, be) → error([])
new_splitGT30(Char(Succ(xux3000)), xux31, xux32, xux33, xux34, Char(Succ(xux4000)), h) → new_splitGT21(xux3000, xux31, xux32, xux33, xux34, xux4000, xux4000, xux3000, h)
new_esEs19(Zero) → new_esEs3
new_addToFM_C0(EmptyFM, xux40, xux41, h) → Branch(xux40, xux41, Pos(Succ(Zero)), new_emptyFM(h), new_emptyFM(h))
new_lt(xux652, xux6500, app(ty_Maybe, cd)) → error([])
new_gt0(Pos(Zero), Pos(Zero)) → new_esEs8
new_esEs16(Zero, xux27930, xux27931, xux27932, xux27933, xux27934, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs14(new_sizeFM(Branch(xux27930, xux27931, xux27932, xux27933, xux27934), ba, bb))
new_addToFM_C10(xux665, xux666, xux667, xux668, xux669, xux670, xux671, False, bd, be) → Branch(xux670, xux671, xux667, xux668, xux669)
new_splitLT30(Char(Succ(xux3000)), xux31, xux32, Branch(xux330, xux331, xux332, xux333, xux334), xux34, Char(Zero), h) → new_splitLT30(xux330, xux331, xux332, xux333, xux334, Char(Zero), h)
new_splitGT10(xux528, xux529, xux530, xux531, xux532, xux533, False, bc) → xux532
new_esEs7 → False
new_esEs21(Neg(xux7560), Pos(xux7530)) → new_esEs22(xux7530, xux7560)
new_esEs21(Pos(xux7560), Neg(xux7530)) → new_esEs22(xux7560, xux7530)
new_primMulNat2(Zero) → Zero
new_gt0(Pos(Zero), Pos(Succ(xux64700))) → new_esEs5(Zero, Succ(xux64700))
new_esEs11(Zero, xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb) → new_esEs12(new_sizeFM0(xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb))
new_emptyFM0(ca, cb) → EmptyFM
new_lt(xux652, xux6500, ty_Char) → new_lt0(xux652, xux6500)
new_splitLT10(xux519, xux520, xux521, xux522, xux523, xux524, Succ(xux5250), Zero, bh) → new_mkVBalBranch5(Char(Succ(xux519)), xux520, xux522, new_splitLT0(xux523, xux524, bh), bh)
new_splitGT0(Branch(xux340, xux341, xux342, xux343, xux344), xux4000, h) → new_splitGT30(xux340, xux341, xux342, xux343, xux344, Char(Succ(xux4000)), h)
new_lt(xux652, xux6500, app(ty_[], dc)) → error([])
new_mkVBalBranch3MkVBalBranch20(xux2790, xux2791, Pos(Succ(xux279200)), xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, False, ba, bb) → new_mkVBalBranch3MkVBalBranch14(xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, xux286, xux287, new_esEs11(new_primPlusNat0(new_primMulNat(xux279200), Succ(xux279200)), xux2790, xux2791, xux279200, xux2793, xux2794, xux2850, xux2851, xux2852, xux2853, xux2854, ba, bb), ba, bb)
new_mkBalBranch6MkBalBranch11(xux731, xux665, xux666, xux6680, xux6681, xux6682, xux6683, EmptyFM, xux730, False, bd, be) → error([])
new_ps(xux668, xux730, xux665, bd, be) → new_primPlusInt(Pos(Succ(Zero)), new_sizeFM(xux668, bd, be))
new_gt0(Neg(Succ(xux65200)), Pos(xux6470)) → new_esEs7
new_primPlusNat0(Zero, Succ(xux160)) → Succ(xux160)
new_primPlusNat0(Succ(xux2100), Zero) → Succ(xux2100)
new_lt(xux652, xux6500, ty_Double) → error([])
new_esEs14(Neg(Zero)) → new_esEs4
new_esEs12(Pos(Succ(xux5200))) → new_esEs1(Zero, Succ(xux5200))
new_primMinusNat0(Succ(xux756000), Succ(xux753000)) → new_primMinusNat0(xux756000, xux753000)
new_gt(x0, x1, app(ty_Ratio, x2))
new_mkBalBranch6MkBalBranch4(x0, x1, x2, x3, EmptyFM, True, x4, x5)
new_mkVBalBranch3MkVBalBranch13(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, False, x11, x12)
new_esEs5(Succ(x0), Zero)
new_splitGT0(Branch(x0, x1, x2, x3, x4), x5, x6)
new_splitLT21(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_mkBalBranch6MkBalBranch3(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8, True, x9, x10)
new_gt(x0, x1, ty_Int)
new_primMulNat(x0)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, EmptyFM, x7, False, x8, x9)
new_primMulNat2(Succ(x0))
new_addToFM_C3(EmptyFM, x0, x1, x2, x3)
new_splitGT30(Char(Succ(x0)), x1, x2, x3, x4, Char(Zero), x5)
new_mkVBalBranch3MkVBalBranch20(x0, x1, Pos(Succ(x2)), x3, x4, x5, x6, x7, x8, x9, x10, x11, False, x12, x13)
new_gt(x0, x1, ty_Float)
new_primMinusNat0(Zero, Zero)
new_lt(x0, x1, ty_Char)
new_mkVBalBranch3MkVBalBranch20(x0, x1, Neg(Zero), x2, x3, x4, x5, x6, x7, x8, x9, x10, False, x11, x12)
new_sizeFM(EmptyFM, x0, x1)
new_mkBalBranch6MkBalBranch3(x0, x1, x2, x3, x4, False, x5, x6)
new_splitLT10(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, x7, x8, True, x9, x10)
new_mkBranch(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
new_mkBranchResult(x0, x1, x2, x3, x4, x5)
new_lt1(x0, x1)
new_esEs9(Neg(Zero), Neg(Zero))
new_primMulNat1(x0)
new_esEs14(Pos(Zero))
new_mkBalBranch6MkBalBranch3(x0, x1, x2, EmptyFM, x3, True, x4, x5)
new_gt(x0, x1, app(ty_Maybe, x2))
new_esEs14(Neg(Zero))
new_mkVBalBranch3MkVBalBranch15(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, True, x12, x13)
new_gt(x0, x1, ty_Double)
new_esEs12(Neg(Zero))
new_esEs12(Pos(Zero))
new_esEs9(Pos(Zero), Pos(Succ(x0)))
new_gt0(Neg(Succ(x0)), Pos(x1))
new_gt0(Pos(Succ(x0)), Neg(x1))
new_esEs16(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_primPlusNat0(Succ(x0), Zero)
new_splitLT21(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_gt0(Pos(Zero), Pos(Succ(x0)))
new_addToFM_C20(x0, x1, x2, x3, x4, x5, x6, True, x7, x8)
new_primPlusInt(Pos(x0), Pos(x1))
new_mkVBalBranch3MkVBalBranch15(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, False, x12, x13)
new_splitLT0(EmptyFM, x0, x1)
new_esEs8
new_gt(x0, x1, ty_Ordering)
new_ps(x0, x1, x2, x3, x4)
new_primPlusNat0(Zero, Succ(x0))
new_primMinusNat0(Succ(x0), Succ(x1))
new_mkVBalBranch5(x0, x1, Branch(x2, x3, x4, x5, x6), Branch(x7, x8, x9, x10, x11), x12)
new_esEs15(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs16(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs7
new_esEs3
new_lt(x0, x1, ty_Float)
new_mkBranch3(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)
new_gt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs11(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_mkVBalBranch10(x0, x1, Branch(x2, x3, x4, x5, x6), x7, x8, x9, x10, x11, x12, x13)
new_mkVBalBranch8(x0, x1, x2, x3, x4, x5, x6, EmptyFM, x7, x8)
new_splitLT10(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_esEs9(Pos(Succ(x0)), Neg(x1))
new_lt(x0, x1, ty_Bool)
new_gt0(Neg(Zero), Pos(Zero))
new_gt0(Pos(Zero), Neg(Zero))
new_esEs9(Neg(Succ(x0)), Pos(x1))
new_primMulNat0(Zero)
new_splitGT21(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_splitGT0(EmptyFM, x0, x1)
new_addToFM0(x0, x1, x2, x3)
new_mkVBalBranch8(x0, x1, x2, x3, x4, x5, x6, Branch(x7, x8, x9, x10, x11), x12, x13)
new_mkBranch0(x0, x1, x2, x3, x4, x5, x6)
new_esEs11(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_addToFM_C10(x0, x1, x2, x3, x4, x5, x6, True, x7, x8)
new_lt0(Char(x0), Char(x1))
new_lt(x0, x1, app(ty_Ratio, x2))
new_primMulNat0(Succ(x0))
new_primPlusInt(Neg(x0), Pos(x1))
new_primPlusInt(Pos(x0), Neg(x1))
new_esEs5(Succ(x0), Succ(x1))
new_esEs9(Neg(Zero), Pos(Zero))
new_esEs9(Pos(Zero), Neg(Zero))
new_esEs13(Succ(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, x6, EmptyFM, x7, False, x8, x9)
new_esEs1(Zero, Succ(x0))
new_splitLT30(Char(Zero), x0, x1, x2, x3, Char(Zero), x4)
new_splitGT4(EmptyFM, x0)
new_esEs9(Neg(Zero), Neg(Succ(x0)))
new_emptyFM0(x0, x1)
new_esEs19(Succ(x0))
new_mkBranch1(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
new_lt(x0, x1, app(app(ty_@2, x2), x3))
new_mkBalBranch6MkBalBranch4(x0, x1, x2, x3, x4, False, x5, x6)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, x6, Branch(x7, x8, x9, x10, x11), x12, False, x13, x14)
new_esEs1(Succ(x0), Succ(x1))
new_gt(x0, x1, app(ty_[], x2))
new_esEs22(Zero, Succ(x0))
new_mkVBalBranch3MkVBalBranch16(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, True, x11, x12)
new_esEs14(Neg(Succ(x0)))
new_splitLT22(x0, x1, x2, x3, x4, x5, x6)
new_mkVBalBranch3MkVBalBranch16(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, False, x11, x12)
new_gt0(Pos(Zero), Neg(Succ(x0)))
new_mkVBalBranch3MkVBalBranch14(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, False, x12, x13)
new_gt0(Neg(Zero), Pos(Succ(x0)))
new_esEs15(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_lt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs1(Succ(x0), Zero)
new_splitLT0(Branch(x0, x1, x2, x3, x4), x5, x6)
new_esEs12(Neg(Succ(x0)))
new_addToFM_C20(x0, x1, x2, x3, x4, x5, x6, False, x7, x8)
new_splitGT21(x0, x1, x2, x3, x4, x5, Succ(x6), Succ(x7), x8)
new_addToFM(x0, x1, x2, x3, x4, x5, x6, x7, x8)
new_mkBalBranch6MkBalBranch11(x0, x1, x2, x3, x4, x5, x6, Branch(x7, x8, x9, x10, x11), x12, False, x13, x14)
new_splitLT30(Char(Succ(x0)), x1, x2, Branch(x3, x4, x5, x6, x7), x8, Char(Zero), x9)
new_sr(Neg(x0))
new_splitLT21(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_mkBalBranch6Size_r(x0, x1, x2, x3, x4, x5)
new_gt0(Neg(Succ(x0)), Neg(x1))
new_splitLT21(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_mkVBalBranch3MkVBalBranch14(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, True, x12, x13)
new_esEs22(Succ(x0), Succ(x1))
new_esEs6
new_gt0(Pos(Succ(x0)), Pos(x1))
new_primPlusInt(Neg(x0), Neg(x1))
new_splitLT10(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_mkBranchRight_size(x0, x1, x2, x3, x4)
new_gt(x0, x1, ty_Bool)
new_gt(x0, x1, ty_@0)
new_mkVBalBranch7(x0, x1, EmptyFM, x2, x3, x4, x5, x6, x7)
new_mkVBalBranch3MkVBalBranch13(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, True, x11, x12)
new_mkVBalBranch6(x0, x1, Branch(x2, x3, x4, x5, x6), x7, x8, x9, x10, x11, x12, x13)
new_addToFM_C10(x0, x1, x2, x3, x4, x5, x6, False, x7, x8)
new_esEs17(x0, Pos(x1))
new_mkVBalBranch3MkVBalBranch20(x0, x1, Pos(Zero), x2, x3, x4, x5, x6, x7, x8, x9, x10, False, x11, x12)
new_mkVBalBranch10(x0, x1, EmptyFM, x2, x3, x4, x5, x6, x7, x8)
new_splitGT10(x0, x1, x2, x3, x4, x5, False, x6)
new_lt(x0, x1, app(ty_[], x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_gt(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(Succ(x0))
new_gt0(Neg(Zero), Neg(Succ(x0)))
new_esEs2
new_esEs14(Pos(Succ(x0)))
new_lt2(x0, x1, x2, x3, x4, x5, x6)
new_gt(Char(x0), Char(x1), ty_Char)
new_mkVBalBranch30(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
new_esEs13(Zero, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_mkVBalBranch7(x0, x1, Branch(x2, x3, x4, x5, x6), x7, x8, x9, x10, x11, x12)
new_sizeFM0(x0, x1, x2, x3, x4, x5, x6)
new_lt(x0, x1, ty_Double)
new_esEs17(x0, Neg(x1))
new_splitLT11(x0, x1, x2, x3, x4, x5, x6)
new_lt(x0, x1, ty_Ordering)
new_mkBalBranch6MkBalBranch4(x0, x1, x2, x3, Branch(x4, x5, x6, x7, x8), True, x9, x10)
new_esEs5(Zero, Zero)
new_sr0(Pos(x0))
new_mkBalBranch6Size_l(x0, x1, x2, x3, x4, x5)
new_esEs9(Pos(Zero), Pos(Zero))
new_esEs21(Neg(x0), Pos(x1))
new_esEs21(Pos(x0), Neg(x1))
new_splitGT22(x0, x1, x2, x3, x4, x5, x6)
new_splitGT30(Char(Succ(x0)), x1, x2, x3, x4, Char(Succ(x5)), x6)
new_lt(x0, x1, ty_Integer)
new_esEs1(Zero, Zero)
new_mkBalBranch6MkBalBranch01(x0, x1, x2, x3, x4, x5, x6, x7, x8, True, x9, x10)
new_addToFM_C0(EmptyFM, x0, x1, x2)
new_splitGT30(Char(Zero), x0, x1, x2, x3, Char(Succ(x4)), x5)
new_esEs10(Neg(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_mkVBalBranch9(x0, x1, Branch(x2, x3, x4, x5, x6), x7, x8, x9, x10, x11, x12)
new_splitGT4(Branch(x0, x1, x2, x3, x4), x5)
new_splitLT30(Char(Zero), x0, x1, x2, x3, Char(Succ(x4)), x5)
new_mkVBalBranch9(x0, x1, EmptyFM, x2, x3, x4, x5, x6, x7)
new_esEs18(x0, Pos(x1))
new_primMinusNat0(Succ(x0), Zero)
new_mkBalBranch6MkBalBranch5(x0, x1, x2, x3, x4, False, x5, x6)
new_lt(x0, x1, ty_@0)
new_addToFM_C0(Branch(x0, x1, x2, x3, x4), x5, x6, x7)
new_emptyFM(x0)
new_lt(x0, x1, app(ty_Maybe, x2))
new_esEs9(Neg(Zero), Pos(Succ(x0)))
new_mkBalBranch6MkBalBranch5(x0, x1, x2, x3, x4, True, x5, x6)
new_esEs9(Pos(Zero), Neg(Succ(x0)))
new_sr(Pos(x0))
new_esEs21(Pos(x0), Pos(x1))
new_esEs4
new_splitGT21(x0, x1, x2, x3, x4, x5, Succ(x6), Zero, x7)
new_mkBranch2(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13)
new_addToFM_C3(Branch(x0, x1, x2, x3, x4), x5, x6, x7, x8)
new_splitGT10(x0, x1, x2, x3, x4, x5, True, x6)
new_primPlusNat0(Zero, Zero)
new_splitLT30(Char(Succ(x0)), x1, x2, EmptyFM, x3, Char(Zero), x4)
new_mkVBalBranch6(x0, x1, EmptyFM, x2, x3, x4, x5, x6, x7, x8)
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_esEs9(Neg(Succ(x0)), Neg(x1))
new_mkVBalBranch5(x0, x1, Branch(x2, x3, x4, x5, x6), EmptyFM, x7)
new_gt0(Neg(Zero), Neg(Zero))
new_esEs9(Pos(Succ(x0)), Pos(x1))
new_mkVBalBranch3MkVBalBranch20(x0, x1, Neg(Succ(x2)), x3, x4, x5, x6, x7, x8, x9, x10, x11, False, x12, x13)
new_splitLT30(Char(Succ(x0)), x1, x2, x3, x4, Char(Succ(x5)), x6)
new_esEs12(Pos(Succ(x0)))
new_splitGT30(Char(Zero), x0, x1, x2, x3, Char(Zero), x4)
new_primMulNat2(Zero)
new_esEs22(Zero, Zero)
new_esEs10(Pos(x0), x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)
new_esEs21(Neg(x0), Neg(x1))
new_gt0(Pos(Zero), Pos(Zero))
new_esEs19(Zero)
new_esEs20(Zero)
new_mkVBalBranch5(x0, x1, EmptyFM, x2, x3)
new_gt(x0, x1, ty_Integer)
new_lt(x0, x1, ty_Int)
new_splitGT21(x0, x1, x2, x3, x4, x5, Zero, Zero, x6)
new_mkVBalBranch3MkVBalBranch20(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, True, x12, x13)
new_splitLT10(x0, x1, x2, x3, x4, x5, Zero, Succ(x6), x7)
new_mkBranch4(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)
new_esEs22(Succ(x0), Zero)
new_lt(x0, x1, app(app(ty_Either, x2), x3))
new_esEs18(x0, Neg(x1))
new_gt(x0, x1, app(app(ty_Either, x2), x3))
new_primMinusNat0(Zero, Succ(x0))
new_esEs5(Zero, Succ(x0))
new_sr0(Neg(x0))
From the DPs we obtained the following set of size-change graphs: